\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{Val} : \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{bool\_val}        : \coqdocvar{Bool}    \ensuremath{\rightarrow} \coqdocvar{Val}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{int\_val}         : \coqdocvar{Integer} \ensuremath{\rightarrow} \coqdocvar{Val}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_val}        : \coqdocvar{Byte}    \ensuremath{\rightarrow} \coqdocvar{Val}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_matrix\_val} : \coqdockw{\ensuremath{\forall}} \coqdocvar{m} \coqdocvar{n}, \coqdocvar{Matrix} \coqdocvar{Byte} \coqdocvar{m} \coqdocvar{n} \ensuremath{\rightarrow} \coqdocvar{Val}\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}